g:OCMon, a, b:|g|. ((a < b)) = (a < b)   

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, gset, OMon, OCMon, goset, a < b, a < b
Definitions	t  T, x:A. B(x), t.1, gset, Mon, AbMon, goset, |p|, OCMon, a < b, a < b
Lemmas	ocmon wf, oset of ocmon wf0, assert of set lt